// html5_download.js
// Add the `download` attribute for each attachment download link.

var potential_download_links = document.getElementsByClassName("f12");
for(var i = 0; i < potential_download_links.length; ++i)
{
	var cur = potential_download_links[i];
	if(cur.id.substr(0, 4) == "att_")
		for(var j = 0; j < cur.children.length; ++j)
			if(cur.children[j].tagName.toLowerCase() == "a")
			{
				var a = cur.children[j];
				a.download = (a.innerText || a.textContent).replace(
					/^\s+|\s+$/g, "");
				break;
			}
}

